es:ES, ff:FIFO, f2f+:F2F+-decls, e:E, sndr, rcvr:ff.C.
([e: sndr is_req   rcvr]  (loc(e) = sndr  Id))
& ([e: rcvr is_ack  sndr]  (loc(e) = rcvr  Id)) 

latex

Definitions	ES, t  T, x:A. B(x), FIFO, F2F+-decls, E, ff.C, is_ack , [e: i p j], loc(e), <a, b>, Id, s = t, is_req  , P  Q, P & Q, A c B, x:A  B(x), A, False
Lemmas	f2f+-property, f2f+Req wf, snd-it wf, f2f+Ack wf, fifoC wf, es-E wf, F2F+-decls wf, FIFO wf, event system wf